COMMENT ⊗   VALID 00017 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.macro bs	⊂ begin indent 2,5 preface 0  ⊃
C00004 00003	.S Basic Research in Artificial Intelligence and Formal Reasoning
C00010 00004	.SS ANALYST - An example of a future application
C00027 00005	.SS Computer aided proofs
C00037 00006	.SS "Accomplishments, Goals and Milestones"
C00038 00007	.SSS Reasonable reasoning
C00043 00008	.SSS Basic artificial intelligence
C00055 00009	.SSS Formal reasoning
C00065 00010	.SSS Reasoning about programs
C00096 00011	.SSS Intelligent access to data bases.
C00103 00012	.SSS Describing other people's files
C00109 00013	.SSS FOL software development
C00112 00014	.SSS Common Business or Military Computer Communication Language
C00122 00015	.SSS A problem solver
C00132 00016	.SS The Formal Reasoning Group
C00137 00017	.bib
C00148 ENDMK
C⊗;
.macro bs	⊂ begin indent 2,5; preface 0;  ⊃
.if false then start "remarks"
Sections
	Notions 
	Inconsistencies 
	Non Mon

DONE:	replace intent by will
DONE:	elaborate comment about Boyer and Moore and DCL

Particular goals
  partition
  Todd Coxeter
  Arith work
  knowledge examples  SandP?

expand Ben

Gio 
other groups
Tarnland
MA
Dave Gifford (258 homework)

maybe prune Reasoning about programs
.end "remarks"
.S Basic Research in Artificial Intelligence and Formal Reasoning

//pers John#McCarthy, Richard#Weyhrauch, Lewis#Creary, Luigia#Aiello, 
Jussi#Ketonen, Ma#Xiwen sra Christopher#Goad, Carolyn#Talcott, Juan#Bulnes, 
Bob#Filman, David#Wilkins, Ben#Moszkowski

Applied research requires basic research to replenish the stock of ideas
on which its progress depends.

The long range goals of work in basic AI and formal reasoning are the same
as described in our previous proposals - to make computers carry out the
reasoning required to solve problems.  Our work over the past few years has
made it considerably clearer how our formal approach can be applied to AI and
MTC problems.  This brings application nearer, especially in the area of MTC.

The point of view of this proposal is substantially the same as that of
our immediately preceding proposal submitted in 1978.  Therefore, the
sections discussing the motivation of that work are substantially taken
from that proposal, with modifications to take into account changes in
viewpoint occasioned by our recent work.  
The section on accomplistments goal, and milestones is new.  
We begin with an outline of our point of view and its relation to applications.  
The work has both theoretical and experimental components.

.SS Directions

Although much of our work is techincal and abstract,  the results will have
important practical applications.  Also, consideration of solutions to
practical problems helps to isolate and clarify some of the technical issues.
For example, consider the problem of designing and effectively using data bases.
For data bases to include many types of information that decision makers
really need will require major advances in representation theory.  Programs
that use the information effectively impose requirements on the
representation and also need new modes of reasoning.  Thus current data
base technology at best allows simple relations to be represented - e.g.
"Smith is the supervisor of Jones."  Additions from current AI techniques
would allow simple generalizations of relations ("Every employee has a
supervisor except the director."), but this leaves a tremendous range of
representation problems untreated:
.skip 1
.bs
1. Mental states - what a person or group believes, knows, wants, fears, etc.

2. Modalities - what may happen, what must happen, what ought to be done, what
      can be done, etc.

3. Conjectures - if something were true what else would be the case.

4. Causality - how does one event follow because of another.
The preconditions of events and the consequences of events.
concurrent events and their laws of interaction and non-interaction.

5. Actions and their modifiers, e.g. "slowly".  

6. Ability - conditions under which a person or group can do something.
.end

Facts of these kinds cannot be adequately represented in data bases at
present, and there are undoubtedly other phenomena essential for
intelligence which have yet to be discovered.  Before such facts can be
incorporated in data bases and question-answering programs in a general
way, basic research must determine the logical structure of these
concepts.

Since much of our research is necessarily very technical, before we
elaborate our recent results and future plans, we will present a
hypothetical example of an applied AI program whose success will depend
on solving the problems we are studying.

.SS ANALYST - An example of a future application

ANALYST scans a computerized %2intelligence%1 data base.  (We italicize
the word "intelligence" when used in the military sense).  It looks for
patterns of information that suggest conjectures about an adversary's
capabilities, intentions, knowledge, beliefs and goals.  When ANALYST
thinks it has found something significant, it informs a human analyst both
about its conclusions and if requested about how it reached them.  Its
forte is examining more data than is possible for a human and guaranteeing
that all possibilities of the kinds it is programmed for are pursued.  The
example is somewhat contrived, because we have emphasized the problems we
are currently studying and ignored others.  Moreover, an ANALYST that
could be programmed on the basis of present knowledge would be very
limited in its capabilities, partly because we have only partially solved
the problems we are studying, but mainly because of problems no-one has
begun to study.

Suppose ANALYST reads in a report from Damascus:
.begin indent 2,2

%2Major Alexei Ivanov went to Damascus airport, bought a ticket to Moscow
for cash, and departed on the next flight to Moscow%1.
.end

ANALYST asks itself why Ivanov did what he did.  Usually it finds
hypotheses that fit a normal pattern of behavior and gains nothing but
further defining the normal pattern.  Let's suppose there is more in this
case.

%2Why did he pay cash%1?  This question arises from a program that looks
for deviations from the normal pattern.  We suppose that the data base
contains a statement that Russians usually buy tickets from their travel
agency Intourist.  The conjecture is then formed that Ivanov is in a hurry
and that some event has required him to go to Moscow suddenly.  The
hypothesis is confirmed by discovering that he had previously accepted an
invitation incompatible with a Moscow trip.

Now suppose that it is known or conjectured that Ivanov is a radar expert.
This leads ANALYST to scan facts about our adversary relationship with the
Russians in the field of radar including the fact that we are trying to
find out the pattern of frequency variation of their radars.  One general
fact in the data base is that when one side finds out the frequency
variation pattern of a radar, the other side wants to change it.
%2Therefore, analyst conjectures that the Russians think we will soon know
the frequency variation pattern of their R111 radar%*.

This simple example poses several problems not handled by present database
programs.  First, present data base systems store particular facts, not
general facts.  General facts usually have to be built into programs or at
least into productions.  Second, the laws that determine what conclusions
can be drawn from facts about knowledge, belief and intentions are
different from those governing non-mental qualities, and present programs
don't use the laws that apply to these %2modal%1 concepts.  Third, the
reasoning required even to conjecture that Ivanov is in a hurry involves
conjecturing that his behavior is normal except in so far as specific
facts suggest abnormalities.  Fourth, many reasoning processes involve
observation as well as reasoning from facts in a data base.  Obtaining the
confirming evidence that Ivanov is in a hurry has that character.
Finally, the pattern recognition required to conjecture from Ivanov's
hurried Moscow trip and the previously known facts that they think we will
soon know their radar pattern is quite different from that done today.  We
shall consider these problems in turn.

.CB Representing general facts

Few existing data base systems represent general facts by entries in the
data base.  For example, ANALYST needs to represent the fact that the
Russians almost always buy their airline tickets from Intourist in such a
way that further deductions can be made and the fact can be modified by
new evidence.  Existing systems represent them by program or by
%2semi-programs%1 like productions.  This works very well for applying the
general facts to particular cases, but it doesn't work well for deducing
new general facts from old ones or representing facts about facts.  In
order to represent general assertions, e.g. Russians buy their tickets
from Intourist, one needs quantifiers, and the most developed logical
system with quantifiers is first order logic.  Even within first order
logic, there are many possible ways of representing a particular kind of
fact, and much further study is required.

.CB Knowledge and belief

The notion %2X thinks Y will soon know Z%1 is not unusually complex when
adversaries try to outwit each other.  It presents problems for machine
fepresentation that haven't been conclusively solved but on which we have
made recent progress.

In order to be useful ANALYST must do more than just represent the above
fact.  It must be able to prove or conjecture it under appropriate
circumstances and it must be able to draw correct conclusions from it -
and not draw incorrect conclusions.  The latter is the more immediate
problem.  Let us use a simpler example.  Suppose we have the sentences
%2Pat knows Mike's telephone number%1 and %2Mike's telephone number is the
same as Mary's%1.  A computerized deduction system that uses the rule that
equals may be substituted for equals might conclude %2Pat knows Mary's
telephone number%1.  This is not a legitimate deduction, even though it
would be legitimate to deduce that Pat dialed Mary's telephone number from
the fact that he dialed Mike's number and the fact that the numbers are
the same.

The fact that substitution of equals for equals is legitimate in some
contexts and not in others has been well known for a very long time.
Correct logical laws for handling such cases have been proposed, but the
presently known solutions have two defects.  First they usually treat only
one such function at a time such as "knows" while real life problems often
mix up several even in the same sentence, e.g. think and know - %2They
think we will soon know ...%1.  Second, each such mental quality requires
modifying the logic.  In a practical case this would be many months work
and might have to be done again and again.

Recently McCarthy has discovered how to represent such facts in unmodified
first order logic.  An improved and extended version of this method
developed by Creary permits the adequate representation of statements
involving any number of different propositional attitudes, nested to any
depth.  The work is described in [McCarthy 1978e] and [Creary 1979], and
will be further developed in the next year.

.CB Conjectures

It has long been recognized that standard logic does not represent the
many kinds of reasoning that people use in forming conjectures.  It now
appears that much human reasoning involves conjecturing that the known
facts about a phenomenon are all the relevant facts.  Thus ANALYST must
conjecture that Ivanov was in a hurry because it has no other explanation
even though it cannot conclusively exclude other explanations.

Strict logical deduction does not permit drawing a conclusion from certain
facts that would be changed if additional facts, supplementing but not
contradicting them, were discovered.  In logic, if a conclusion follows,
it will still follow when more facts are added.  Humans, on the other
hand, are always drawing this kind of conclusion.  We now think that
machines must also reason this way, and that programs confined to strict
logical reasoning must either be unable to draw conclusions or they must
use axioms so unqualified that they are false.

McCarthy has recently found a partial solution to this problem [McCarthy
1978d].  An axiom schema of first order logic called the %2circumscription
induction schema%1 can be used to represent in a flexible way the
conjecture that the entities that can be shown to exist on the basis of
the information in a certain data base are all the relevant entities that
exist.  The flexibility comes from the fact that the set of information
conjectured to be all the relevant information is readily changed.  Martin
Davis of New York University has helped in the mathematical formulation of
circumscription.

Circumscription is a fully formal mode of reasoning and can be programmed
for a computer.  On the other hand, it is not %2valid%1, i.e.  it can yield
false conclusions from true premises.  This is to be expected, because
mathematicians have proved the completeness of the rules of inference of
first order logic; hence all the infallible inferences that do not depend
on the interpretation of the premises and/or conclusion have already been
provided for.  So, programs that use circumscription cannot be certain
that their conclusions are as good as their premises, and must be made
capable of withdrawing conclusions arrived at by circumscription that turn
out to be unacceptable, without necessarily also renouncing the premises.
This will make them more like humans - getting increased power at the
price of fallibility.

.CB Patterns

Many of the patterns ANALYST will have to recognize do not fall into the
categories so far treated in AI work.  For example, explaining an unknown
activity of an adversary requires conjecturing a goal and its relation to
other goals, a belief structure that makes the goal seem desirable and
attainable, and a means of attaining the goal that gives rise to the
observations.  Present AI pattern recognition programs find patterns in
observed data rather than introduce new entities in order to explain the
data.  McCarthy is developing a general notion of pattern, and Wilkins is
using chess to develop some advanced notions of strategic pattern.

Our object in raising these problems is not to show that present database
efforts are misdirected.  In our opinion, the problems being explored are
entirely appropriate.  However, it is necessary to look further ahead and
provide the basic research foundation for more advanced database work.
The same basic research will also support other intelligent system and
program verification advances. 

.SS Computer aided proofs

The study of representation of facts and modes of reasoning has an
experimental as well as a theoretical aspect.  The long run test of the
usefulness of a means of representation or a mode of reasoning is its
contribution to the success of question answering and problem-solving
programs.  However, this is a slow way of testing newly developed
concepts, because it often requires the creation of a whole new data base
format.  New concepts can be studied much more quickly if we can test
their consequences directly in relative isolation.

The main tool in making a computer follow reasoning is a %2proof
checker%1.  Ours is called FOL (for %3F%2irst %3O%2rder %3L%2ogic%1) and
checks proof in a system of first order logic that has been enhanced in
many ways.  We use this tool to formulate the facts involved in an
intellectual problem and check that our representation is adequate to
solve the problem.  The facts we are studying are general facts about
situations and events and actions and goals, the effects of actions that
manipulate physical objects, and the facts about sources of information
such as books, computer files, people and observation that are necessary
in order for a program to obtain the information required to solve
problems.

Actually, FOL goes beyond just proof-checking, because it includes
substantial elements of proof-finding and these are to be enhanced.  We
are incorporating many known methods of proof-finding in FOL, so that a
user can get the machine to prove what it can and do the rest himself.

In addition to its applications to AI, proof-checking is used to verify
that computer programs meet their specifications.

That proof-checking by computer might have important applications was
first proposed by McCarthy in 1960 [McCarthy 1963a], and Paul Abrahams
wrote an M.I.T. Ph.D.  thesis in 1962 implementing such a checker.
Unfortunately, the computers, our understanding of logic, and our
understanding of mathematical theory of computation were all inadequate at
the time for the proposed application to proving correctness of programs.
The next proof checker may have been one using resolution written by
[McCarthy 1965].  FOL is this laboratory's fifth proof-checker following
McCarthy's, one by W. Weiher that we weren't prepared to use at all, one
by Whit Diffie that was used for some small problems, and the LCF proof
checker of Robin Milner and Richard Weyhrauch that was extensively used to 
prove theorems about recursively defined programs.  An example of the use of 
LCF in the study of programming language semantics is given in [Aiello 1977].
FOL takes into account this previous experience and is designed to be able 
to check very large proofs; some proofs longer than 2000 steps have been
checked.  Other proof checkers include one by Bledsoe at the University of
Texas, one at the Stanford University Institute for Mathematics in the
Social Sciences that is used to teach logic and set theory and the Boyer and
Moore system at SRI.  Robin Milner has also made a new version of LCF at 
the University of Edinburgh.

FOL is an interactive program, each step is checked as soon as it is
typed, though proofs can also be taken from files.  The logic is a version
of that described in [Prawitz 1965].  It has been shown by mathematicians
that if you start with any of the well-known axiomatizations of set
theory, e.g. ZF or GB, and additional axioms expressing the definitions of
various mathematical domains, then there exist derivations of all the
well-known mathematical theorems.  However, these derivations are
generally extremely long, because the usual logical systems do not
incorporate as primitives all the modes of reasoning actually used.  FOL
contains many features that allow more natural and efficient expression of
facts and reasoning.  In particular the semantic attachment feature of FOL
allows the user to create in addition to a first order theory, some
computable part of the intended model of that theory.  The total
environment is known as an L/S pair (or language/simulation structure
pair).  In this environment proofs can be carried out by the usual methods
of deduction, by computation in the model, or by combinations of both.

We have really just begun work on finding out what formal derivations in
existing formal systems look like.  The comparison of these to the proofs
of mathematicians will certainly lead to formalisms that are more like
mathematical practice.  Many of the proofs we have already done use a
version of set theory due to [Kelley 1955].  We observe that our proofs
are much longer than informal proofs partly because mathematical logicians
have reduced the number of concepts in set theories to a minimum in order
to make metamathematics, i.e., proofs about the formal systems, easier.
One of our goals is a "heavy duty" set theory that will make functions and
partial functions available to the user as basic concepts.  Another major
requirement is to allow the user access to a library of already proved
theorems.  Of course, there is no need to prove all these theorems in FOL;
we can just copy them out of the literature.  The difficulty is that we
cannot yet change notation and basic definitions as easily as a
mathematician can in switching from one book to another.

Our experience has certainly shown the basic feasibility of computer-checked
mathematical proofs as all the cases we have tried have gone through, albeit
with much more work than is required for an informal proof.
In some cases we have made good progress in deveoping techniques for doing
proofs that are indeed very similar to the corresponding informal proof.

.SS "Accomplishments, Goals and Milestones"

In the course of this contract we will study two main areas:
the epistemological problems of AI and mathematical theory of computation.
A lot of this work but not all will be directed at using FOL as a tool
to study general problems of epistemology.
In the following sections we describe some of our recent accomplishments,
ideas for research and some specific tasks related to these ideas
that we will carry out in the next two years.
.SSS Reasonable reasoning

In previous proposals we have written about the inadequacies of existing
formalisms to represent the reasoning of individuals in a way that is
close to their informal explanations.  We have said things about what
cannot be said or understood by current formalisms.  The point of this
section is to explain that in fact substantial improvement has been made
in the direction of expressing certain kinds of reasoning.  A fair amount
of work is expected to be done to illustrate this success.  We are pleased
about two areas.  One is our preliminary experiments with FOLISP.  The
proofs described in [Talcott 1979] are clear, understandable and are largly
%2of the same size%* as the informally written out proofs.  The second
area is elementary arithmetic and algebra. This effect is achieved by the
specific interactions of the FOL features designed by Weyhrauch and
implemented by us all over the past several years.  The importance of this
is that we have found a way of arranging formal ideas so that the quality
of the conversations that we can have with FOL are approaching (in limited
areas) the level of informal discussion we can have with people.  We hope
to widen the illustrations to include the heavy duty set theory mentioned
below and some of the McCarthy work on reasoning about belief.  This work
will be pursued by McCarthy, Weyhrauch, Talcott, Aiello, Kim and Ward (The
latter two are students interested in FOL and contributing to our effort).

.cb goals

⊗  The work on FOLISP will be continued and expanded.  We will demonstrate
the practical viability of our approach to reasoning about programs by
making a version of FOLISP which will be used by %2beginning programers%*
in elementary courses on LISP programming at Stanford.  continuing 
1979 - 1981.

⊗  We will represent many examples from textbooks on elementary high school
algebra in the FOL style.  The idea here is not to build a program that will 
%2do%* the problems of high school algebra, but rather to build a system that 
has an understanding of algebra.  We will work out an example using this 
system in which it will reason about which heuristics should be used to 
factor simple algebraic expressions.  Fall 1979.

⊗  Chapter 3.1 of [Mendelson 1963] will be rewritten as if he had had FOL
available to him when he wrote it.  We believe that all of the informal
proofs that appear in this chapter can be expressed exactly as they appear 
in his book.  There is no other existing AI representation system that can
do this.  Winter 1979.

.SSS Basic artificial intelligence

.cb Reasoning about knowledge 

We believe that a lot of our common sense reasoning depends on our ability to
understand and reason about what we know and what we know about what other
people know.  Richard Weyhrauch has several objections to how reasoning
about knowledge is usually dealt with in both the AI and philosophical
literature.  One of his strongest objections is to any principle of the
form - if a person knows that "P implies Q" and he also knows "P" then he
knows "Q".  It seems to Weyhrauch that this is simply false.  It means, for 
example, that every mathematician who knows the axioms of set theory know 
whether Fermat's "theorem" or the Riemann Hypothesis is true.  This seems 
to him to be false, but can be proved from any theory of knowledge that
contains principles like those above.  These principles occur in many well
known theories of knowledge.  Weyhrauch believes he has a theory of
knowledge that allows one to carry out ordinary reasoning about knowledge
without such a principle.  This requires the use of metatheory and a
discussion of the amount of resources a person is willing to devote to
finding out the consequences of what he already knows.

Lewis Creary is currently developing an alternative approach to reasoning
about propositional attitudes which shares Weyhrauch's concern to avoid
unrealistic idealizations concerning the logical closure of belief sets.
The representation scheme used is McCarthy's first-order theory of
individual concepts and propositions [McCarthy 1978e], extended by Creary
to permit adequate representation of iterated propositional attitudes, and
the semantically simpler representation of quantified propositions and
"definite-description" concepts of individuals.  The method of reasoning
about the knowledge, beliefs, and desires of an organism is
knowledge-based, and uses a program's own ordinary inferential apparatus
to "simulate" the reasoning of the given organism.  The method thus avoids
a need for redundant re-representation of information about propositions
at higher levels in the hierarchy of concepts.  This framework for
representation and reasoning is described in [Creary 1979].  The sort of
information that the framework is meant to handle is illustrated by
the content of this sentence: %2 "Ivanov believes that none of the authors
of the coded message knows that the code has been broken."%* The features
of this sentence that are of special interest here are i) the nesting or
iteration of propositional attitudes ("knows" within the scope of
"believes"), ii) the occurrence of a quantifier ("none") within the scope
of a verb of propositional attitude ("believes"), and iii) the occurrence
of definite descriptions (e.g., "the coded message") within the scope of
"believes".

In other work not yet ready for publication, Creary has proposed a new
analysis of the notion of epistemic feasibility.  This is a key idea
needed in planning for the availability of knowledge.  Thus, in
constructing a plan for the opening of a safe, a problem-solving robot has
to verify, not only that it will be physically able to manipulate the dial
appropriately at the right time, but also %2that it will know the
combination of the safe%1 at that time.  Without this knowledge of the
combination, the action of opening the safe will not be %2epistemically
feasible%1 for the robot.  A formal analysis of this idea is needed to
give automatic problem-solvers a general capacity to infer an agent's
ability to perform an action from the agent's possesion of appropriate
knowledge (among other things).  The new analysis of epistemic feasibility
promises to solve a problem posed in [McCarthy 1977b] as follows:  "The
most immediate AI problem that requires concepts for its successful
formalism may be the relation between knowledge and ability.  We would
like to connect Mike's ability to open %2safe1%1 with his knowledge of the
combination.  The proper formalization of the notion of can that involves
knowledge rather than just physical possibility hasn't been done yet."

Besides exploring these ideas, we are applying to AI problems
McCarthy's knowledge formalism, as integrated
with his treatment of propositions and individual concepts.  In particular
we are trying to formalize the effect of learning on knowledge of quantified
sentences.  A correct formalization of the effect of learning
and especially learning
about other people's knowledge will be required for the proposed %2Analyst%1
system.

.cb goals

⊗  McCarthy's knowledge formalism will be integrated with his treatment of
propositions and individual concepts.  Examples will be tried using FOL.
This problem will be attacked by McCarthy and Creary.  continuing 1979-1981.

⊗  Creary will continue the development of his ideas on representation and
reasoning in the context of designing the new problem solver described in
a later section of this document.  continuing 1979-1980.

⊗  McCarthy's knowledge formalism will be extended to represent the
effects of learning on knowledge of quantified sentences.
The problem being studied is one called S and P, about two 
mathematicians' knowledge of the sums and products of two numbers and their
knowledge of each other's knowledge or lack of knowledge of the problem.
An original formalization of this problem by McCarthy has  been
improved by Ma Xiwen.  Problems remain with correctly describing
the effects of one person learning what another person
knows.  We expect to have a correct formalism for this learning
by Spring 1980.

⊗  We will return to the three wise men problem and use FOL to represent 
proofs in a formalism suggested by Ma Xiwen.  Fall 1979.

.cb Situations

What is a situation?  What is an action?  A lot of work in AI has gone into
these two questions.  Weyhrauch has proposed that when doing common sense 
reasoning and talking about a situation, we are really talking about a %2theory%*
of the world.  This is in contrast with the point of view that a situation is an
instantaneous state of the world.  FOL builds data structures (LS structures)
which Weyhrauch claims are a natural mechanization of the idea of theory.  If you
take the above point of view - that what we actually do in common sense reasoning
is to reason about our theories of the world - then the metamathematical machinery 
of FOL is exactly the thing you need to reason about situations.  In the 
metatheory actions can simply be considered functions on situations (i.e. 
theories).  This idea has been worked on by Carolyn Talcott and Richard 
Weyhrauch in a reformulation of some classical AI robotics puzzles.  We will 
continue this line of investigation and write up current work.

.cb goals

⊗  The work begun by Talcott and Weyhrauch on the Keys and boxes problem
will be completed.  We expect to produce a system that can be queried by
novice users about this problem.  Summer 1980.

⊗  Work will continue on formalizing concurrent action.  This involves
giving rules for achieving goals when several people or machines or other
causes of events are acting at once.  None of the current AI formalisms
handle it even in the simplest case when the different actors do not
interact.  In our opinion, it is one of the most important unsolved problems
in the theory of artificial intelligence.  continuing 1979-1981.

.SSS Formal reasoning

.cb Meta reasoning

A large number of the projects we expect to carry out during this contract 
will use the metatheoretic machinery of FOL.  This is one of the central 
themes of these projects.  For this purpose we will need to do futher
development on the part of the FOL system that we call META.  One of the 
goals of this work is to produce a description of FOL in its own language.
This is a continuing effort and contributes importantly to almost everything 
we are doing.  The three sections below describe several important topics in
AI that this work addresses.  The importance of our work is that it provides
a uniform framework in which to address these problems.  In addition, we will
test the developement of META by using it to formalize some recent developments
in constructive mathematics.  The work on set theory will also be used in FOLISP.
This area will be worked on by Ketonen, Weyhrauch, Talcott and Aiello.

.cb goals

⊗  Our goal is to have a solid axiomatization of META by early 1981.  This
axiomatization, the FOL evaluator and our work on reasoning about programs
will then facilitate a synthesis of the FOL reasoning system into a 
unified whole that will act as its own evaluator.

⊗  We have an example of a single metatheorem that can be applied in three
different contexts.  1) algebra. 2) propositional logic. and 3) set 
theory.  The ability to state such general principles is an illustration
of how we expect to get leverage by having meta theory around.  We will
describe this metatheorem in detail and demonstrate its use in the three
areas mentioned above.  Winter 1979.

⊗  Until recently there have been no reasonable axiomatizations of set 
theory that allowed for the formation of sets of arbitrary things.  Recent
developments of logicians have produced two new possibilities: one called
T0 and developed by S. Feferman and one called KPU developed by J. Barwise.
There is no existing AI systems except FOL capable of using these theories
because to use them effectively requires the availability of a large amount
of metatheoretic machinery.  We will express both of these theories in FOL
and do experiments to determine their relative merits.  by Summer 1980.

.cb The introduction of new ideas

Every system comes designed with some initial set of ideas.  A question we 
are addressing is: how can we organize such a system that when new ideas
or new ways of looking at old ideas are discovered by a user that they can
be incorporated into the system %2without%* the system designer having to
start again.  Two questions arise.  First, how can new ideas be defined to
the system and in what language should they be stated?  Second, how can we
know that the new ideas don't conflict in some round about way with the 
ones we are already using?

The FOL system already has some facility for a user to introduce new 
definitions.  The literature of logicians contains several additional
ideas about how to facilitate these kinds of extensions to existing 
systems.  They are: 1) showing that the introduction of certain
definitions on form alone are conservative extensions of a given theory,
2) the Beth definability lemma ststes when implicit definitions can be
turned into explicit ones, 3) the theory of general inductive definitions,
4) the idea of a comprehension principle.  We will examine these ideas 
and see whether any of them are useful in a technical sense for the 
problems of AI.

Another important related question for AI is:  how can these new ideas be
learned and incorporated in a way that they can be %2used%* by a AI system.
An example of this kind of learning is given in [Weyhrauch 1978b] (section 9.1).
We will explore how this idea of learning works in more detail.

.cb Reasoning about inconsistencies 

One problem not yet faced in AI is how to reason about inconsistencies.  One
of the observations that is frequently make is that humans continually have
contradictory information and so intelligent systems will also have to deal
with such incoherent data.  One of the reasons for having metatheoretic 
reasoning available in FOL is that one can talk about properties like 
consistency.  Imagine that we have a theory called %3LS%* and some amount of
reasources %3r%*.  We can introduce a predicate, %3consist(r,LS)%*, into 
the metatheory which says that the resources %3r%* are not enough to prove
that the theory %3LS%* inconsistent.  This is a formal way of saying that
we can't detect any inconsistencies in %3LS%*. This idea is similar to to
the trick Rosser used to remove the restriction of omega consistency from
Godel's first incompleteness proof.  We will work out examples
illustrating how to use this idea.  This research interacts with our 
interest in non-monotonic reasoning and circumscription as both of these 
techniques can sometimes invalidate facts previously thought to be true.

.cb Non-monotonic reasoning

The usual systems of logic have the property that if P proves Q, then P
together with any other facts also proves Q.  Examples of reasoning that
appear to contradict this property appear in the literature of AI.  One
approach to these problems is the idea of circumscription introduced in
[McCarthy 1977b].  An alternative proposal of [McDermott and Doyle 1978]
was to introduce "consistency" as a modality.  In the section above we
mentioned a new way we will deal with the ideas of consistency, that is,
not as a modality but by a direct attack in the metatheory.  This same 
directness can be applied to circumscription at the cost of introducing 
the metatheory machinery for discussing what it means to be the intended
model of a theory.  We hope to continue the work on circumscription and 
explore the alternative formulation using metatheory.

.SSS Reasoning about programs

Our work in reasoning about programs is a combination of mathematical
theory of computation and formal reasoning.  It has immediate applications
to such problems as program verification and synthesis.  We also plan to
use the results as a part of a foundation for solving more general
reasoning problems.  We describe here three areas of research on programs.

.cb The Elephant programming language.

McCarthy has recently discovered a new language called Elephant for
writing sequential programs.  It has two interesting properties.

First, the programs are represented as collections of sentences of first
order logic.  In this respect Elephant resembles Lucid and Prolog.
However, the Elephant representation is more direct than these and permits
proving properties of the program without any special mathematical theory
of computation - merely the program itself and an axiomatization of the
data domain.  The method involves replacing each variable of the program
and the "program counter" by a function of time and writing recursion
equations for this function.  The Elephant style of describing algorithms
is in some sense the opposite of the method of describing recursive
programs due to Cartwright and developed by [Cartwright and McCarthy
1979a,b].  Namely, the recursive function method describes the output
function in terms of simpler cases and therefore can be called
%2top-down%1, while the Elephant method works from an initial state and
desribes how it is transformed.  Presumably the two methods will be found
to be complementary.

The second property of Elephant makes it a higher level
language than any in  present use at the cost of requiring a heuristic
program as a compiler.  Namely, an Elephant statement can refer to
the past without specifying any data structure in which information
about the past is stored.  As an informal example, an Elephant program
can say, %2"A passenger has a reservation if he has successfully made
one and hasn't cancelled it"%1.  The point is that the program prescribes
no data structure for remembering reservations, and the compiler must
decide that cancelled reservations and unsuccessful attempts to make
reservations do not have to be remembered.  It seems to us that the
italicized statement is one that is likely to be made by a person
describing in English what he wants a computer to do.  Unless he
is a programmer, it may not even occur to him that some data
structure must be created and maintained in order to get the desired
behavior.

Elephant programs that refer to the past in this way are
nevertheless collections of sentences of logic, and their properties
can be stated and proved without an additional theory of computation.
Concurrent processes can also be described in Elephant.  In particular,
the fact of non-interference of processes can be specified without
giving a method of achieving it, thus leaving achieving non-interference
up to the compiler.

More sample programs need to be written before it can be
determined whether Elephant or Elephant features are a convenient
way of writing programs.  If the answer to this question is positive,
the next step is the design of a compiler.  Since the design of
data structures will probably turn out to be a substantial mathematical
problem in general, an Elephant compiler will be a heuristic program
that recognizes certain cases and doesn't always give an acceptable
result without the help of putting in some data structures explicitly.

Before this it may be desirable to gain some experience in
transforming Elephant programs mathematically, e.g. in transforming
programs that refer to the distant past into programs that refer
only to the immediate past but in which data structures are explicit.

⊗A preliminary writeup on Elephant is included as Appendix A.


.cb Formalizing properties of LISP programs.

In the past programming has been done in a way that it is separate from 
any attempt to verify the properties of programs.  We feel that it is
important to develop systems in which programs can be
constructed, evaluated and in analysed.  One of our main tools for
this research is the FOL system described above.

There are several reasons why this research is new and interesting:

Although there are many systems which currently do program verification,
(e.g. [Boyer and Moore 1975], [Luckham 1977])  each of these have strong
restrictions built into them.  Boyer and Moore can only deal with programs
that thay can prove wil  terminate.  The McCarthy formalism does not have
this problem.  The Luckham system has the problem that it can only deal
with one program at a time.  One way of leveraging program proving effort
is to prove general properties of collections of similar programs.  These
theorems can then be used over and over again.  FOL
has the expressive power to overcome both of these difficulties.  This
generality has an associated cost.  Namely, you 
must explicitly explain to FOL every idea that you want to use.  This may
require a large initial investment.  The compensation is that once you
have invested in this initial cost the range of problems that you can
discuss using FOL is very large compared with other systems.  For example,
with the exception of LCF ([Milner 1972], [Gordon 1977]), we believe that 
all existing verification systems have a fixed programming language that 
they can deal with.  Because in FOL programs are represented in terms of 
their abstract syntax we can, for example, speak of both PASCAL programs 
and LISP programs in the same FOL language.  Since we also can talk about
functions, as well as programs, we can say that two programs in two
different programming languages compute the same function on the integers.
If you want to prove this using standard program verification methodology
it requires the use of two systems to verify that same specifications are
met.  One area where this is particularly useful is in proving the
correctness of compilers.  Here we need to express properties of both the
source and target languages.  The proof of the correctness of a compiler
for the expression language described in [McCarthy-Painter 1967] has 
already been carried out in FOL.

McCarthy has found Cartwright's thesis [Cartwright 1977] the key to
implementing his long term goal of expressing recursive program
definitions as sentences of logic.  While McCarthy's older approach
required using a logic of partial functions and predicates which
introduces many complications, Cartwright's approach uses ordinary first
order logic.  Using it permitted McCarthy to simplify his earlier ideas
and apply them to moderately complicated programs.  Besides an exposition
of Cartwright's formal ideas separated from his proof-checker, [Cartwright
and McCarthy 1979b] contains a minimization scheme that characterizes a
recursive program as the minimal solution of the Cartwright functional
equation, a characterization of the verification methods of inductive
assertions (Floyd) and subgoal induction (Manna-Pnueli and
Wegbreit-Morris) as axiom schemata, and a greatly simplified analog of the
Goedel-Kleene method of representing recursive functions in first order
logic.  This method of representation shows that any sentence involving
LISP programs could be translated automatically into a sentence involving
only the basic Lisp functions and the relation of one list being a tail of
another.  This shows that their first order theory of recursive of
programs is complete relative to the data domain, i.e.  no further theory
of programs is logically required.

McCarthy has discovered how to use the theory of functions that he has
recently developed to prove intensional properties of functions.  This
idea is new and we believe that it opens up a large area for important
future research.  It facilitates in a theoretically sound way of reasoning
about things that would otherwise require a complicated discussion of the
details of an interpreter.  The work on a cost compiler 
mentioned below under goals are examples of this idea.

.cb Goals

We have begun 
experimenting using FOL as an interactive environment in which programs
can both be executed or their properties described and proved.  This 
system is based on the ideas of [Kleene 1936, 1952], [Cartwright 1977], 
developed in [Cartwright and McCarthy 1979b].  
This system is called FOLISP and its current state is described in 
[Talcott 1979].  We have chosen to treat the programming language LISP,
but the ideas apply to any language.  We intend to continue building 
and refining this system.  In its current state it has been used by 
students to prove some simple properties of programs they have written.  
We plan two direction of development of this system.  One is to express
and verify the correctness of more complicated programs using the 
existing formalism.  We have two particular examples in mind.

⊗ Most of the examples treated so far have trivial correctness proofs, and
the interest lies in proving mathematical properties of the function
computed by the program.  
We will represent a LISP program to partition a list into %2n%* sublists 
in all possible ways in FOL, define the notion of partition of a list,
and prove that the program computes all and only partitions of a list.
The interesting issue in this example is that the program in not just a 
direct translation of the natural statement of what is meant by "partition" 
and by "all partitions".
This work will be done by Talcott in 1979.

⊗ For the second example we will implement
the Todd-Coxeter algorithm for enumerating cosets of groups presented
by finite collections of generators and relations and prove its correctness.
This algorithm is an important part of many of the existing programs that
do group theoretic computations.  In order to state and prove its correctness
we will need to axiomatize the theory of groups and express the relevant
group theoretic notions in FOL, as well as representing the LISP program
as a collection of first order sentences.  This will be a very non-trivial
example,  and will demonstrate the feasibility of using our methods
for problems of genuine practical interest.  
This work will be done by Talcott, 1979-80.

The second direction of development of the FOLISP system will be to
refine and extend the formalism
in order to increase the expressive power and to develop techniques
simplifying proofs, making them more natural and making the system
even more accessible to non-expert users.   This work will
involve using the metamathematical facilities of FOL. 

⊗ We will axiomatize LISP programs including the primitive operations,
and the COND, LAMBDA, PROG, and boolean constructs.  


⊗ We will extend the usual syntax of first order language (the language of FOL)
to include first order %4λ%1-expressions, program like terms and a recursive function
definition construct.  This will require
some theoretical work to understand the impact of such extensions on the
class of models and the proof theory of our system.  The reason for making
this extension is to provide a natural way of expressing facts about programs
and the corresponding functions.  

⊗ We will axiomatize an inpterpreter for the LISP programs, define a mapping
from the domain of LISP programs to a class of recursive functions definitions,
and prove the soundness of this mapping.
This will allow us to formalize the representation of programs as functions
(and to automate it).  We will also define a mapping from a subclass of
recursive function definitions to the domain LISP programs thus facilitating
the ability to switch between programming and reasoning modes.  The mappings
between programs and functions will be part of the metatheory of our theory of
LISP programs and functions.

⊗ We will define a notion of computation (relative to an interpreter).  
This will provide the ability to express and prove facts about how a
program works.  This includes the standard problems of space and time
complexity as well as reasoning about intermediate states of computation, etc..
This will also provide a formalization of the methods developed by 
McCarthy and Moszkowski for representing intensional properties of a program
via a "derived" program.
We note that different interpreters will result in different computations
for a particular program.  Although we intend to fix on a particular interpreter
for most of our work, we have the ability to define alternate interpreters
and reason about the differences between them.

The above tasks will be carried out by Weyhrauch and Talcott in the Fall of 1979.

⊗ Ben Moszkowksi will continue his work on representation of intensional
properties of programs.  He will prove the correctness of a "cost 
compiler" that converts a program into a "derived" program that computes
some property of the computation of the original program such as the
number of times a given operation is executed, the number of times the
program calls itself recursively, etc..  He will also develop an idea
for an alternate method of representation, which is to modify the interpreter
to compute the desired property rather that than execute the program.
He will prove various properties of the modified interpreter.  The proofs
will be carried out in FOL using the exended FOLISP formalism as 
described above.  This will be done during the academic year 1979-80.

⊗ We will have the ability to axiomatize and thus use (via reflection)
whatever verification methodology that we choose.  This includes, for 
example, both Scott induction or the Floyd-Hoare inductive assertion 
method.  Currently we can express and use simple structural induction
schemata (such as numerical, list or S-expresion induction) in FOLISP.
When the FOLISP formalism is more fully developed, we will 
express,prove the soundness of various verification techniques.
In particular we will represent the following formalisms: 
.begin verbatim

	(1) The minimization schema (Kleene[1952], McCarthy[1978b]) 
	(2) Computation Induction (Scott, Gordon[1977]) 
	(3) Structural induction (Burstall, Boyer-Moore[1975])
	(4) Invariant Assertions (Floyd-Hoare,Luckham[1977])
	(5) Intermittent Assertions (Manna-Waldinger[1978])
	(6) Sub-goal Induction (Morris-Wegbreit[1976])
.end

⊗ We will develop and prove the soundness of some heuristics for proving
various classes of statements about programs and recursively defined functions.  
Some examples are:
.begin nofill

(1) Proof of termination of certain programs based on the syntactic form of the
program.

(2) Automatic proof of theorems using structural induction schemata.

(3) Reduction of more complicated proofs to a list of non-trivial
lemmas.  (Thus relieving the user of the bookkeeping and repetitious parts
of carrying out proofs in FOL that are currently necessary.)
.end
These heursitics can be expressed as theorems in the metatheory of the theory
of LISP and can be used via the FOL reflection facility as derived proof rules.
They will facilitate the use of the FOLISP system by both expert and non-expert
users.  We also view this as work towards find the correct notions and
data structures for representing reasoning in a natural way.  Thus it is
connected with the work on reasonable reasoning.

⊗ We will also be able to express properties of classes of programs and 
relations between programs.
The kind of theorem we have in mind is:  for all LISP programs, p, if they 
are of the recursive form 

f(x) ← if x=0 then k else h(f(x-1),x-1)

then there is a corresponding iterative program, p', of the form

.begin verbatim

f(n) ← f1(n,n,0)

f1(m,n,ans) ← if m=0 then ans 
                 else f1(m-1,n,h(ans,n-m))
.end

which computes the same function.

The system we will build can deal with this example in two ways.  First
we will be able to state and prove this theorem.  This is already more than
existing verification systems are capable of doing.  Secondly, by using
reflection and the metatheory we will be able to construct the later
out of the former in a completely automatic way.  This is a form of
automatic program synthesis using program transformations, [Burstall and
Darlington 1976].  This can not be done in a system that cannot deal 
with classes of programs.  We will express and prove some theorms of 
the sort given above and experiment with using them.

The above work will be carried out as a continuation of the FOLISP 
development in 1980-81.

.cb Normalization of proofs.  

It was discovered by logicians in the 1930's that special kinds of proofs
of arithmetic statements about the existence of numbers could be used to
actually find those numbers.  To try and be more concrete, suppose that we
have a proof that for every number x there is another number y such that a
complicated relation holds between x and y.  For example, it was proved in
Euclid that for every positive integer x there is some other integer p
that is a prime number and is bigger than x.  The technique of logicians
called %2normalization%* tells us that there is a mechanical procedure
(i.e. a computer program) that by looking at this proof it can find a
program which given any x will compute the required p.  This is a kind of
automatic program construction, where the specification of the program is
the proof that such a program should exist.  Until recently this fact has
gone completely unnoticed by the computer science community.  We are doing
experiments to determine whether this technique is feasible and at all
useful to computer science.  As a side effect we hope to shed some light
on problems of interest to logicians.

Chris Goad implemented the Prawitz normalization routines.  He has
applied them to proofs of several theorems of arithmetic, among them
the proof that there are infinitely many primes.  
Since the formula proved states that for each number there is a prime
larger than that number,
this proof serves as a program which computes a prime larger than its input.
Goad is working with Professor Georg Kreisel who is one
of the world leaders in the branch of logic called proof theory.

.cb Goals

⊗ The existing work needs to be written up.  Fall 1979.

⊗ The work of producing a computationally efficient implementation of
normalization has just been completed.  We plan a series of experiments
whose purpose is to assess the practical applicability of proofs as
descriptions of computation.  We have chosen a class of two dimensional
packing problems as our test domain.  The work involves building up a
collection of proofs which establish computationally useful facts about
the domain, and investigation of the computational efficiency aspects of
these proofs - for example, comparisons of the efficiency of different
proofs of the same theorem. On-going work - present - 1981.

⊗ There is a collection of transformations on proofs which may be used to
improve the efficiency of the proof viewed as a description of
computation.  Some of these transformations are a part of the
normalization process itself, and as such are implemented in the currently
existing code.  Others, particularly those applicable to various schemes
of induction, have not been studied previously.  We plan theoretical study
of the class of such transformations.  Implementation of some such
transformations is planned; their practical utility will be assessed as
part of the packing experiments.  Fall 1979, Winter 1980

.SSS Intelligent access to data bases.

In our previous proposals and in the ANALYST example above we have described
how the pure epistemological research that we have been doing will have 
an important impact on data base research as we discover how to deal with
the complicated issues of representation described in the ANALYST example.

In a more direct sense the current FOL system can be used to address 
questions of current interest.  Discussions with the data base experts Gio 
Wiederhold and D. Sagalowicz have convinced us that the following ideas 
embodied in FOL can presently be useful to data base researchers.

1.  A theory of the data.  FOL is an ideal environment to describe a theory
of a data base.  A straight forward description of the data will contain
as a subpart a relational model of the data base.  The availability of full 
logic gives you a hiearchical description as well. 

2.  Defined relations.  In the section above on AI we described the 
importance of being able to define new notions when we reason about 
something.  In terms of data bases it is the question of how can we 
define new relations out of old ones.  How are these stored and can
they be of any use other than answering the current query.  FOL 
facilitates the making and saving of new relation definitions in a
symbolic form that can then be further used to reason about the 
information in the data base.

3.  Consistency checking.  Using the metatheoretic machinery of FOL
one can formalize the rules and notions needed to do sophisticated
consistency checking on the data.  If theorem proving is necessary
then the heuristics for controling this (even down to discussing 
resource allocation) can be described to FOL.

4.  Using theorem proving to do search optimization.   The idea here
is that by having a theory of how the data is stored, that reasoning 
about how to access it is facilitated by the same machinery as 
reasoning about the data itself.

5.  Search heuristics.  In [Weyhrauch 1978b] we show how various proof 
techniques can be described in FOL.  We then go on to describe how
the heuristics for using these rules can also be formalized.  The
reflection facility of FOL then "implements" these heuristics as a 
matter of course.

6.  Models of users.  In addition to having theories of the data,
a data base should either have or be able to form theories of
its users.  This is another form of its ability to have more than 
one theory of the data (one for each type of user).  This can be 
done by the same theory building machinery.

7.  Reorganization of data.  Once we can reason about how a user views
the data then we hope to determine (reason about) whether the way in
which the data is stored is appropriate.

In each of the cases above we have described a potential use of an FOL
like system as applied to data bases.  The importance of FOL here is
not that it solves the problems of what kinds of consistency checking 
neede to be done, or how to reorganize a data base, but rather it
provides a way of looking at the entire problem in a uniform way. 
There is only one system.  The specialization of this uniform reasoning
expert is then an engineering task.  

The literature already contains the growing awareness that powerful
reasoning systems can be effective in dealing with data bases. We have not
yet carried out this specialization in any particular case, but would like
to do some beginning work along this line.  It is expected that this work
will be done by Luigia Aiello.

.cb goals

⊗  To give a clear demonstration of the connection between the relational
model of data bases and the formal systems used by FOL.  Spring 1979.

⊗  To explain how existing data bases work can be formulated in our terms,
and then address the issues mentioned above.  Summer 1980.

⊗  To build a small relational data base to illustrate these ideas.  Fall
1980.

.SSS Describing other people's files

This part of the proposal is to develop a system for describing
existing files over whose format the describer has no control.

The increase in communication facilities between computers
produces many opportunities for organizations to use each others files,
but few of the opportunities have been realized.  For example, Lawrence
Berkeley Laboratory has a file of census data, but it is not a routine
operation for programs all over the country to use this data.  Another
example is that almost every ARPAnet installation maintains a local file
of names and addresses, but it requires special knowledge for a user of
Stanford's computer to get at the address and telephone files at the
M.I.T. Artificial Intelligence Laboratory.

One approach to solving such problems is for everyone to agree to
use common formats for certain kinds of files, i.e. for one data base
scheme to "conquer the world".  This isn't going to happen.  Files are
developed at differing times at different technological levels and with
different hardware.  Co-ordination within a single installation is difficult
to achieve, and larger scale co-ordination is achieved only in connection
with the development of new systems.

This proposed work is based on accepting the idea that many installations
and many applications within installations will develop their own file formats.
To cope with this we propose to develop a widely applicable system for
formally describing existing file formats.  Given such a description,
a general program can interpret it in order to extract information from
or even put information into other people's files.

Consider the address and telephone files at the various
laboratories.  If we do our job well, each such file will be describable
in our File Description Language (FiDL).  A program can then be asked for
the telephone number of Patrick Winston at M.I.T., will read the file
description, call M.I.T. on the ARPAnet and extract the desired
information.  Since most of the installations include additional
information in the file much of which is not interesting to outsiders,
FiDL should provide for partial description of files.

The Lawrence Berkeley Laboratory census files provide
an interesting different problem.  We want to describe them in such a way
that a user anywhere on the ARPAnet can ask a local program for the
1970 population of Pittsburgh and get an answer from a program that
knows about the LBL file.  The user himself need not know where the
information is coming from.   However, the LBL census file is intended
to be interrogated by a human interactively and not by a computer.  Therefore,
FiDL must provide for the formal description of the interaction method
so that the program using it can pretend to be a human and engage in a
suitable dialog with the LBL program.

We propose to devote one research associate to this problem for the two
year period of the contract.  He may be assisted by graduate students of
suitable talents and interests.  The work will result in a program that
can be used from anywhere in the ARPAnet and will extract information from
files on the ARPAnet for which descriptions have been made.  We plan to
use the address and telephone files as our first experimental domain.
Costs are detailed in the budget.

.SSS FOL software development

We are currently going though a period of intense discussion about some
of the user engineering problems of FOL.  Thus some of our time will be
spent making FOL more friendly to the user.  Our interest has been
partially prompted by many requests to use FOL by people at other ARPA
sites.  This has been the result of the publications of [Weyhrauch 1978b].
We have not commited ourselves in any way to supply anyone with any
resources but, we wish to facilitate remote demonstrations.
With this in mind we will:

⊗  Make FOL usable from a teletype.  That is provide a mode that is
accessible to people without the Stanford character set.  December 1979.

⊗  Completely redo FOL's facility to show information about its
current state.  This will include facilities that currently do not 
exist to help users debug their use of the meta theory.  January 1979.

⊗  Produce software which interfaces this new showing facility with
our XGP, in order to have more readable local output.  This is 
particuliarly important if students are to use FOLISP.  January 1979.

A second kind of software development will go into actual features of
the system.  These will include

⊗  Making the introduction of definitions more convenient.  March 1980.

⊗  We will implement a new memory management scheme into FOL to increase
the size of the experiments that we can perform.  This is particularly
important as the real power of metatheory lies in having many
simultaneously active theories.  November 1980.

⊗  We will augment the FOL parser and the evaluator to include
McCarthy's idea of first-order lambda terms.  This will be important 
to the work on MTC.  September 1980.

⊗  A rule of conjecture will be added to FOL generating the
circumscription schema for a collection of sentences with respect to a
predicate.   June 1980.

.SSS Common Business or Military Computer Communication Language

It is increasingly necessary for computer systems to
communicate with each other electronically without human intervention.
For example,  The inventory computer at an airbase should be
able to requisition supplies from the inventory computer at
some general supply base which in turn should be able to deal
with computers belonging to commercial firms.  The full cost-saving
benefits of computerized data bases often substantially depend
on direct communication between computers without going through
humans.  Thus if an inventory control system merely tells a clerk
to type out a purchase order for some supplies and that purchase
order is received by another clerk who types its contents into
a computer, most of the costs and delays remain.  Whatever degree
of human monitoring of simple transaction is wanted is best achieved
by having the computer prepare the communication for approval
or disapproval by a human at the appropriate level of authority.

Such inter-computer communication exists today but always
by specific treaty between the two communicators.   For example,
the Internal Revenue Service will accept the information on
W-2 forms on magnetic tape from employers provided it is in a
form prescribed by the Service.  Also the Fleet Data System
exchanges information between ships on what airplanes and ships
are known to the various ships of the fleet, and this information
has a format that was defined when the Fleet Data System was
designed.

As an alternative to designing the communication at the
same time the computer systems using the information are designed,
we propose study a %2Common Business Communication Language%1.
This language would provide semantics and syntax for many kinds
of military and commercial business messages.  The language would
be extensible and usable by all kinds of computer systems.  One
would expect that the designers of all kinds of inventory systems,
requisition systems, purchasing systems, reservations systems and
data base systems would implement communication with other systems
using this language.

Our interest is not in the electronic level of communication,
i.e. we are not proposing yet another effort to standardize modems,
frequencies, error detection and correction, etc.  Instead we aim
at the semantic content of the messages.
Thus we wish to standardize such messages as

How many F15s do you have, and how many are in working order?

Please send 500 spare part number 314159265 to arrive
before 19 January by authority of Colonel XYZ.

My order number 271828 has not arrived.  What is the current
delivery situation.

What kinds of pencils do you sell, and when could you
deliver 1000 gross number 2 yellow pencils?

The main problem is not to standardize the grammar of such messages.
In fact we already have a plan for doing that.  Rather the problem
is to standardize the semantics of a wide class of messages so that
programs can be designed to produce them and interpret them properly.

This immediately confronts us with the problems of find a
useful subset of natural language and standardizing its semantic
content.  Thus consider the part of the language used to express
military requisitions.  In its simplest form, what is being requisitioned
is a quantity of an item identified by a stock number.  More generally,
substitutions are possible.  A delivery method must be specified, but
it may be partially left open to depend on circumstances.  The authority
for the requisition or purchase must be specified, and the price
stated or requested or a reference to a prior agreement must be
made.  Even this limited class of messages presents difficulty
at our present level of understanding of natural language.

Indeed the Common Business Communication Language requires the
solution of a different set of problems from those involved in
putting natural language front ends on otherwise conventional
programs.  In the latter case the problem is to say in English
what we already know how to say in %2computerese%1, whereas our
problem is how to say in the most convenient language for a computer
things that computers have heretofore not said at all.  In our opinion,
this semantic problem has greater scientific interest and greater
practical importance than the well-studied syntactic problems.
From both the scientific and the practical point of view, the interesting
thing about natural language is not how its syntax differs from
computer languages but rather the fact that it is possible to
say in natural language things that computer languages can't express
at all.  This proposal is an example of something that cannot be
said in computer languages but much too complicated an example
for study at the present stage of science.

We believe that the business communication language problem
is at the right level of difficulty from a scientific point of
view and promises practical application.

There is a tendency for system designers to propose to
solve the communication problem by designing (say) an entire
military business system and design the communication simply
as part of the larger problem.  Such attempts to "conquer
the world" are doomed to failure.  It always happens that part
They require getting everyone to agree to switching to a fixed
system at some definite time in the future.  This locks up the
technology and often disrupts successful local solutions of
local problems.  A common business communication language opens
up the possibility of modularizing the overall system.  Different
companies or different parts of government can proceed at different
rates as their present hardware and software become obsolete.  When
they need to procure new hardware or software, they can do so
according to the best buys currently available using newly developed
techniques.  They are not bound to someone's grand plan of ten
years ago.

Some preliminary thoughts on the Common Business Communication
Language are included as Appendix B of this proposal.  The level
of effort proposed is one Research Associate for the two year
period.  Details are given in the budget.

.SSS A problem solver

Recent progress by McCarthy and Lewis Creary in formalizing knowledge
about propositional attitudes, by McCarthy in formalizing the new method
of circumscription, and by Creary in formalizing the notion of epistemic
feasibility suggests that problem solvers using the new ideas may be
able to treat naturally problems that are inaccessible to or awkward
for previous general problem solvers.  These problems include those
of planning for the availability of knowledge (see section 2.4.2 above),
and those whose solution requires the making of reasonable, but
fallible, conjectures (see section 2.2 above).  Checking this requires
experiment, and Creary has begun studies leading to the design of a
problem solver that implements these ideas.

.cb goal

⊗ We plan to write a problem solver that uses knowledge in its data base
about the knowledge, beliefs, and desires of various organisms to achieve
its goals.  It will be able to reason about the epistemic feasibility of
actions, both for itself and for others.  It will also be able to use
circumscription to express assumptions that the data it possesses are
sufficient to solve a problem.  Naturally, many details of our current
design ideas are either tentative or unspecified at this early stage of
the research.  We do not yet know whether we will have to write a problem
solver from scratch or whether we can get an adequate research tool by
modifying an existing system.

.cb motivation

In general, we wish to keep our thinking in touch with the prime criterion
of value for ideas in artificial intelligence -- their contribution to the
successful performance of problem-solving, question- answering, and
learning programs.

More specifically, we wish to be able to test realistically (and, when
possible, to demonstrate) the problem-solving power of ideas, approaches,
and techniques developed within the AI & Formal Reasoning Group.

Still more specifically, we wish to investigate the heuristic
adequacy of the new ideas mentioned above concerning

.begin indent 0,3; preface 0; nojust;
a) the representation of facts about knowledge, belief, and desire,

b) the analysis of epistemic feasibility,

c) the form of some conjectural reasoning.
.end

A related, but somewhat different, motivation is the desire to determine
where the weakest threads are in the fabric of current AI heuristic
technology -- especially in relation to the solution of problems of the
type characteristically investigated by our group.
 
.cb Design Goals

.begin indent 0,3;
I.  The problem solver should provide a convenient and effective test bed
and development tool for the research conducted by members of the AI &
Formal Reasoning Group.  Accordingly, it should emphasize (but not
overemphasize) the role of logic in problem solving, and should facilitate
the evaluation and improvement of ideas and techniques developed within
the group.

II.  The design should reflect the present state of the art in problem
solving.  We don't want to re-invent anything, or (still worse) to have
readily avoidable deficiencies in the program.  We want to provide the
best possible problem-solving environment in which to try out our ideas.

III.  The problem solver should be readily revisable, in order to
facilitate and encourage experimentation with a number of different
problem-solving designs.  This ease of revision is essential if the
problem solver is to function over a significant period of time as a truly
useful research tool.  The way to achieve this goal is to design the
program in such a way that those conceptually independent features of it
which might be subject to change (memory retrieval algorithm, problem
solving control structure, etc.,) are variable independently of one
another in the program, and are represented by easily variable program
elements such as production rules, parameter tables, etc.  The implication
of this approach is that we should try to design, not a particular problem
solver, but a system or framework for problem solving that can be
"programmed" to instantiate any of a large number of particular problem
solvers.  Concern with this issue need not bog us down in system building,
however; it should be possible to start by writing a particular problem
solver with built-in generalization points.  The important thing is to
keep this design goal in mind from the beginning.
.end

.cb Relation to FOL

The elementary parts of FOL and the proposed new problem solver are the
tools of different, complementary approaches to research in artificial
intelligence.  In its simplest form, FOL may be viewed as the
proof-checking component in McCarthy and Hayes's [1969] "Missouri program"
(MP), and as such is a tool of epistemological research; such research may
(and probably should) be carried quite some distance in abstraction from
heuristic issues before attempts are made to implement ideas in a full
problem-solving context.  On the other hand, the proposed new problem
solver is a version of McCarthy and Hayes's "reasoning program" (RP), and,
in the presence of basic FOL, can be reserved for study of the primarily
heuristic aspects of a given class of problems.  It is to be expected that
research economies will be achieved by using the two programs thus in
tandem, since it will probably be cheaper to check the epistemological
adequacy of ideas with FOL than with the problem solver.  Moreover, this
division of labor will permit individual researchers to focus closely on
manageable subparts of a given AI problem.

.cb Basic Approach

Our basic approach will be to use state-of-the-art AI techniques to
construct an implementation of John McCarthy's "Advice Taker" program more
or less along the lines first laid down in his paper "Programs with Common
Sense" [1959], and extended in McCarthy and Hayes [1969] and subsequent
papers by McCarthy.  A preliminary review of the Advice-Taker design in
the light of currently available AI techniques suggests that the basic
design is sound, and that prospects for a successful implementation are
good.

.cb Goals

⊗  Preliminary study completed and direction decided - April 1980.

⊗  System design for problem solver and preliminary experiments - August 1980.

.SS The Formal Reasoning Group

John McCarthy is Professor of Computer Science and has worked in the area
of formal reasoning applied to computer science and artificial
intelligence since 1957.  He is working on the logic of knowledge and
belief, the circumscription mode of reasoning, formalizing properties of
programs in first order logic and a general theory of patterns.

Richard Weyhrauch is Research Associate in Computer Science, has a Ph.D.
from Stanford in mathematical logic and has worked on mathematical theory
of computation and the development of proof-checkers.  He is in charge of
the work on FOL.

Lewis Creary is Research Associate in Computer Science, received his
doctorate from Princeton University in philosophy, and has been concerned
with epistemology, semantics, logic, and a computational system for
inductive inference.  He is working on epistemological problems of AI, and
on the design of the proposed problem solver.

Jussi Ketonen is a visiting Research Associate from the faculty of the University
of Hawaii.  He recieved his Ph.D. from University of Wisconsin in mathematical 
logic and in interested in the mechanizable aspects of formal reasoning.

Luigia Aiello is a visiting scholar from Italy. She has worked on mathematical
theory of computation. She is mainly interested in the use of metamathematics 
in FOL, and in its applications to reasoning about data bases.

Ma Xiwen is a visiting scholar from China.  He is interested in reasoning
in natural language.   He has been working on formalizations of problems
that involve learning and reasoning about what others know.

Juan Bulnes is studying combinatorial proofs in FOL, trying to make them
as short as informal proofs.

Robert Filman is working on combining observation with reasoning, using a
chess problem as an example.  In the next period, he will work on a method
of formally describing pre-existing data bases in such a way that an
interpreter of the description can extract information from
them.

Chris Goad is studying the form and complexity of proofs.  He is interested
in the problem of converting proofs of existence into programs and in
analysing when doing the proof might be preferable to writing the program.

Ben Moszkowski is working in proving properties of compilers.  He is interested
in studying a sequence of compilers each slightly smarter than the previous one
and in developing methods for proving properties based on the simple 
transformations that relate the compilers in the sequence.  These ideas will
be formalized in FOL and related to the formal framework being developed
by C. Talcott.  They apply to a very general notion of compiler and also
relate to work on intesional properties of programs.

Carolyn Talcott is working on formalizing the theory of LISP functions and programs
in order to develop a system for reasoning about programs in which many diverse
techniques of proving properties of programs can be expressed, used and studied.

David Wilkins is working on the formalization of an abstract notion of pattern.
.bib

[Aiello 1977]
Aiello, L., Aiello, M. and  Weyhrauch, R.W.,
"Pascal in LCF: Semantics and Examples of Proofs", Theoretical Computer 
Science, 5 (1977).

[Boyer and Moore 1975]
Boyer, R.S., and Moore, J.S.,
"Proving Theorems About LISP Functions",
JACM, 22 (1975), pp. 129-144. 

[Burstall and Darlington 1976]
Burstall, R. M., and Darlington, J., "A System which Automatically
Improves Programs", Acta Informatica, 6 (1976), pp. 41-60.

[Cartwright 1977]
Cartwright, R., "Practical Formal Semantic Defintion and Verification 
Systems", Ph.D. thesis, Computer Science Department, Stanford University, 
Stanford (1977).

[Cartwright and McCarthy 1979a]
Cartwright, R. and McCarthy, J.,
"First Order Programming Logic",
Proc. of the 6th Annual ACM Symp. on Principles of Programming Languages,
San Antonio, Texas, (January 1979).

[Cartwright and McCarthy 1979b]
Cartwright, R. and McCarthy, J.,
"Recursive Programs as Functions in a First Order Theory",
Stanford AI Memo AIM-324, (March 1979).

[Creary 1979]
Creary, Lewis G., "Propositional Attitudes: Fregean Representation and Simulative
Reasoning," forthcoming in Proceedings of the Sixth International Joint Conference
on Artificial Intelligence, to be held in Tokyo, Japan, August 1979.

[Filman 1978]
Filman, R.,
"The interaction of Observation and Inference", Ph.D. Thesis, 
Stanford AI Memo AIM-327, (June 1979).

[Goad 1978]
Goad, C. A.,
"Monadic Infinitary Propositional Logic: A Special Operator",
Reports on Mathematical Logic, 10 (1978).

[Gordon 1977]
Gordon, M., Milner, R. and Wadsworth, C. "Edinburgh LCF", Department
of Computer Science Internal Report CSR-11-77, University of Edinburgh, Edinburgh 
(1977).

[Kelley 1955] 
Kelley, J., <General Topology>, Van Nostrand, Princeton (1955).

[Kleene 1936]
Kleene, S. C., "General Recursive Functions of Natural Numbers",
Math. Ann., 112 (1936), pp. 727-742.

[Kleene 1952]
Kleene, S. C., <Introduction to Metamathematics>, Van Nostrand, Princeton (1952).

[Luckham 1977]
Luckham, D., "Program Verification and Verification-oriented 
Programming", IFIP-77, North-Holland, Amsterdam (1977).

[McCarthy 1959] 
McCarthy, J., "Programs with Common Sense", 
Proc. Int. Conf. on Mechanisation of Thought Processes, Teddington, England, 
National Physical Laboratory, (1959).

[McCarthy 1963a]
McCarthy, J., "A Basis for a Mathematical Theory of Computation",
in  Braffort, P. and Herschberg, D. (eds.), <Computer Programming and Formal
Systems,> North-Holland, Amsterdam (1963).

[McCarthy 1963b] 
McCarthy, J., "Towards a Mathematical Science of Computation",
in  Popplewell, C.M. (ed.), <Information processing:  Proceedings of
IFIP Congress 62,> North Holland, Amsterdam, (1963).

[McCarthy 1964] 
McCarthy, J., "A Formal Description of a Subset of ALGOL",
in  Steel, T.B., Jr. (ed.), <Formal Language Description Languages
for Computer Programming,> North Holland, Amsterdam (1966).

[McCarthy 1965] 
McCarthy, J., "Proof-Checker for the Predicate Calculus",
Stanford AI Memo AIM-27, March 1965.

[McCarthy and Painter 1967] 
McCarthy J. and Painter, J., "Correctness
of a Compiler for Arithmetic Expressions", in Schwartz, J.T. (ed.),
<Proc. of a Symposium in Applied Mathematics, 19 -- Mathematical
Aspects of Computer Science,> American Mathematical Society, Providence,
Rhode Island (1967).

[McCarthy and Hayes 1969]  
McCarthy, J. and Hayes, P., "Some Philosophical Problems from the
Standpoint of Artificial Intelligence", AIM-73, November 1968; also in
D. Michie (ed.), <Machine Intelligence,> American Elsevier, New York, (1969).

[McCarthy 1977a]
McCarthy, J.,
"Another SAMEFRINGE", SIGART Newsletter No. 61, (February 1977), p4.

[McCarthy 1977b]
McCarthy, J.,
"Epistemological Problems of Artificial Intelligence",
Proc. of the 5th International Joint Conference on Artificial Intelligence,
(1977) (Invited Paper).

[McCarthy 1978a]
McCarthy, J.,
"History of LISP",
Proc. of the ACM Conf. on History of Programming Languages (1978).

[McCarthy 1978b]
McCarthy, J.,
"Representation of Recursive Programs in First Order Logic",
Proc. of the International Conference on Mathematical Studies of Information
Processing,  Kyoto, Japan (1978).

[McCarthy 1978c]
McCarthy, J.,
"Ascribing Mental Qualities to Machines", to be published in 
<Philosophical Perspectives in Artificial Intelligence>, Martin Ringle (ed.),
Humanities Press (1978), also available as Stanford AI Memo AIM-326, (March 1979).

[McCarthy 1978d] 
McCarthy, J.,
"Circumscription Induction - A way of Jumping to Conclusions", forthcoming.

[McCarthy 1978e] 
McCarthy, J.,
"First Order Theories of Individual Concepts and Propositions",
Stanford AI Memo AIM-325 (March 1979).

[McCarthy 1978f]
McCarthy, J., Sato, M., Hayashi, T. and  Igarashi, S.,
"On the Model Theory of Knowledge",
Stanford AI Memo AIM-312, April 1978.

[McDermott and Doyle 1978]
McDermott, D., and Doyle, J. "Non-Monotonic Logic I", A.I. Memo 486,
MIT, Boston (1978).

[Manna and Waldinger 1978]
Manna, Z. and Waldinger, R., "Is SOMETIME Sometimes Better than ALWAYS?
Intermittant Assertions in Proving Program Correctness", CACM, 21 (1978),
pp. 159-172.

[Mendelson 1963]
Mendelson E., <Introduction to Mathematical Logic,> Van Nostrand, Priceton, 1963.

[Milner 1972]
Milner, R. G. M., "Logic for Computable Functions: Description of
a Machine Implementation", AIM-169, Stanford AI Lab, Stanford (1972),
Available as α<Arpanet:SAILα> LCFMAN.RGM[AIM,DOC].

[Morris and Wegbreit 1976]
Morris, J. H., and Wegbreit, B., "Subgoal Induction," CACM, 20,
(1976), pp. 209-222.

[Prawitz 1965] 
Prawitz, D., <Natural Deduction,> Almqvist & Wiksell, Stockholm, (1965).

[Talcott 1979]
Talcott, C.L.,
"Reasoning About LISP: a Tutorial in Formalizing Properties of LISP Programs
and Their Proofs."
Stanford AI Memo, forthcoming, (1979).

[Weyhrauch 1977]
Weyhrauch, R.W.,
"A Users Manual for FOL", Stanford AI Memo AIM-235.1, (July 1977).

[Weyhrauch 1978a]
Weyhrauch, R.W.,
"Lecture Notes on Logic and AI",  Prepared for the Summer School on Foundations
of Artificiial Intelligence and Computer Science, Pisa, Italy, (June 1978).

[Weyhrauch 1978b]
Weyhrauch, R.W.,
"Prolegomena to a Theory of Mechanized Formal Reasoning", 
Stanford AI Memo AIM-315 (December 1978).

.end